Added help line for dev-docs target.

diff --git a/Makefile b/Makefile
index 498be57835af48904ba6105be7c872221058ea75..ea52d8c98c55cf5e0bb1e508dca98794ff64f22f 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -126,7 +126,7 @@ help:
        @echo '  install-xen      - build and install the Xen hypervisor'
        @echo '  install-tools    - build and install the control tools'
        @echo '  install-kernels  - build and install guest kernels'
-       @echo '  install-docs     - build and install documentation'
+       @echo '  install-docs     - build and install user documentation'
        @echo ''
        @echo 'Building targets:'
        @echo '  dist             - build and install everything into local dist directory'
@@ -136,7 +136,8 @@ help:
        @echo '  tools            - build and install tools'
        @echo '  kernels          - build and install guest kernels'
        @echo '  kbuild           - synonym for make kernels'
-       @echo '  docs             - build and install docs'
+       @echo '  docs             - build and install user documentation'
+       @echo '  dev-docs         - build developer-only documentation'
        @echo ''
        @echo 'Cleaning targets:'
        @echo '  clean            - clean the Xen, tools and docs (but not'